\begin{tabbing}
$\forall$$T$:Type, ${\it as}$,${\it bs}$:($T$ List).
\\[0ex]no\_repeats($T$; ${\it as}$)
\\[0ex]$\Rightarrow$ no\_repeats($T$; ${\it bs}$)
\\[0ex]$\Rightarrow$ \=((${\it as}$ = ${\it bs}$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($\forall$$x$:$T$. ($x$ $\in$ ${\it as}$) $\Leftarrow\!\Rightarrow$ ($x$ $\in$ ${\it bs}$))\+
\\[0ex]$\wedge$ ($\forall$$x$,$y$:$T$. l\_before($x$; $y$; ${\it as}$; $T$) $\Leftarrow\!\Rightarrow$ l\_before($x$; $y$; ${\it bs}$; $T$))))
\-\-
\end{tabbing}